$\forall$$i$, $x$:Id, $T$:Type, $v$:$T$. AtomFree(Type;$T$) $\Rightarrow$ @$i$ $x$ initially $v$:$T$ $\Vdash$ ${\it es}$.@$i$ $x$ initially $v$:$T$